package tests;

import operateurs.Et;
import operateurs.Ou;
import base.Atome;
import base.Formule;
import quantifieurs.Existe;
import quantifieurs.PourTout;
import termes.Variable;

public class TestTransportQuantificateur {
	public static void main(String[] args) {
		// 1) QQx A(y)  -->  A(y)
		System.out.println("/////Test 1 : /////");
		Formule test1 = new PourTout(new Variable("x"), new Atome("A", new Variable("y")));
		System.out.println(test1);
		test1 = test1.transportQuantificateurs();
		System.out.println(test1);

		System.out.println("/////Test 2 : /////");
		Formule test2 = new Existe(new Variable("x"), new Atome("A", new Variable("y")));
		System.out.println(test2);
		test2 = test2.transportQuantificateurs();
		System.out.println(test2);

		// 2) QQ x, QQ y A(x)  -->  QQx, A(x)
		System.out.println("/////Test 3 : /////");
		Formule test3 = new PourTout(new Variable("x"), new PourTout(new Variable("y"), new Atome("A", new Variable("x"))));
		System.out.println(test3);
		test3 = test3.transportQuantificateurs();
		System.out.println(test3);
		
		System.out.println("/////Test 4 : /////");
		Formule test4 = new Existe(new Variable("y"), new Existe(new Variable("x"), new Atome("A", new Variable("x"))));
		System.out.println(test4);
		test4 = test4.transportQuantificateurs();
		System.out.println(test4);

		// 3) QQ x, A(x)  ^  QQ x, B(x)  -->  QQx,(A(x) ^ B(x))
		System.out.println("/////Test 5 : /////");
		Formule test5 = new Et(new PourTout(new Variable("x"), new Atome("A", new Variable("x"))), new PourTout(new Variable("x"), new Atome("B", new Variable("x"))));
		System.out.println(test5);
		test5 = test5.transportQuantificateurs();
		System.out.println(test5);

		// 4) E x, A(x)  ^  E x, B(x)  -->  E x,(A(x) ^ B(x))
		System.out.println("/////Test 6 : /////");
		Formule test6 = new Ou(new Existe(new Variable("x"), new Atome("A", new Variable("x"))), new Existe(new Variable("x"), new Atome("B", new Variable("x"))));
		System.out.println(test6);
		test6 = test6.transportQuantificateurs();
		System.out.println(test6);

		// 5) (QQ x, A(x)) ^ B(y)  -->  QQ x, (A(x) ^ B(y)
		System.out.println("/////Test 7 : /////");
		Formule test7 = new Et(new PourTout(new Variable("x"), new Atome("A", new Variable("x"))), new Atome("B", new Variable("y")));
		System.out.println(test7);
		test7 = test7.transportQuantificateurs();
		System.out.println(test7);

		// 6) (QQ x, A(x)) v B(y)  -->  QQ x, (A(x) v B(y)
		System.out.println("/////Test 8 : /////");
		Formule test8 = new Ou(new PourTout(new Variable("x"), new Atome("A", new Variable("x"))), new Atome("B", new Variable("y")));
		System.out.println(test8);
		test8 = test8.transportQuantificateurs();
		System.out.println(test8);
	}
}